package edu.msoe.se3811.jmlunit.code.wordnum;

public class WordNumber {
	
	private /*@ non_null spec_public */ String value;
	
	private /*@ spec_public */ static String[] numValues = new String[] {
			"zero","one","two","three","four","five",
			"six","seven","eight","nine","ten"
	};
	
	/**
	 * No-argument constructor ("zero" value).
	 * 
	 */
	/*@
	  @ public normal_behavior
	  @ ensures getNumValue() == 0;
	  @ assignable value;
	  @*/
	public WordNumber () {
		this("zero");
	}
	
	/**
	 * Construct from String value.
	 * @param value String with a valid numeric value.
	 */ 

	/*@
	  @ public normal_behavior
	  @ requires value != null;
	  @ requires (\exists int i; 0 <= i && i < numValues.length; numValues[i].equals(value));
	  @ ensures this.value.equals(value);
	  @ assignable this.value;
	  @ also
	  @ public exceptional_behavior
	  @ requires value != null;
	  @ requires !(\exists int i; 0 <= i && i < numValues.length; numValues[i].equals(value));
	  @ signals_only IllegalArgumentException;
	  @ assignable \nothing;
	  @ also
	  @ public exceptional_behavior
	  @ requires value == null;
	  @ signals_only NullPointerException;
	  @ assignable \nothing;
	  @*/
	public WordNumber (/*@ nullable @*/ String value) {
		
		if(value == null)
			throw new NullPointerException("value was null");
		
		//Make sure that value is a valid number
		boolean found = false;
		for (int idx = 0; !found && idx < numValues.length; idx++) {
			if (numValues[idx].equals(value)) {
				found = true;
			}
		}			
		
		if(!found)
			throw new IllegalArgumentException("Invalid value.");
		
		this.value = value;
	}
	
	/**
	 * Add two WordNumber values.
	 * @param value String with a valid numeric value.
	 */

	/*@
	  @ public normal_behavior
	  @ requires other != null &&
	  @          (this.getNumValue() + other.getNumValue() <= 10);
	  @ ensures (\result).getNumValue() == this.getNumValue() + other.getNumValue();
	  @ assignable \nothing;
	  @ also
	  @ public exceptional_behavior
	  @ requires other == null;
	  @ signals_only NullPointerException;
	  @ assignable \nothing;
	  @ also
	  @ public exceptional_behavior
	  @ requires other != null && this.getNumValue() + other.getNumValue() > 10;
	  @ signals_only IllegalArgumentException;
	  @ assignable \nothing;
	  @*/
	public WordNumber add (WordNumber other) {
		
		if(other.getNumValue() + getNumValue() > 10)
			throw new IllegalArgumentException();
		
		int val1 = this.getNumValue();
		int val2 = other.getNumValue();
		WordNumber sum = new WordNumber(numValues[val1 + val2]);
		return sum;
	}	
	
	/*@
	  @ public normal_behavior
	  @ ensures numValues[(\result)].equals(value);
	  @
	  @*/
	
	public /*@ pure */ int getNumValue () {
		int numVal = 0;
		boolean found = false;
		for (int idx = 0; !found && idx < numValues.length; idx++) {
			if (numValues[idx].equals(value)) {
				numVal = idx;
				found = true;
			}
		}
		return numVal;
	}

	/*@
	  @ also
	  @ public normal_behavior
	  @ ensures (\result).equals("WordNumber["+value+"]");
	  @
	  @*/
	public String toString() {
		String stringValue = "WordNumber["+value+"]";
		return stringValue;
	}

}
